| Definitions | t  T, Id, s = t, Prop, {T}, P  Q, False, P   Q,  A, Type,  x.A(x),  x:A. B(x),  x. t(x), a:A fp B(a), Top, x:A B(x), IdDeq, x dom(f),  b, Void, f || g, True, A & B, P & Q, b,  , Knd, ,  x:A. B(x), KindDeq, x : v, a = b, SQType(T), s ~ t, Atom$n,  T, @loc x initially v:T, Realizer, A || B, p  q, type List, x,y,z. t(x;y;z), IdLnk, State(ds), x,y,z,w,v. t(x;y;z;w;v), DeclaredType(ds;x), x:A B(x), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z,w. t(x;y;z;w), es realizer ind, f(a), {x:A| B(x) }, P  Q, P Q, Unit, left+right, es realizer ind Rrframe compseq tag def, es realizer ind Rinit compseq tag def, i=j, Rsends-T(x1), Rsends-dt(x1), Rsends-l(x1), Rsends-knd(x1), Rsends?(x1), Reffect-T(x1), Reffect-knd(x1), Reffect?(x1), Rrframe-L(x1), Rpre-a(x1), Rpre-ds(x1), Rrframe-x(x1), Rrframe?(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-g(x1), Rsframe-tag(x1), Rsframe-lnk(x1), Rsframe?(x1), Reffect-ds(x1), Raframe-L(x1), Reffect-x(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Rframe-x(x1), Rframe?(x1), Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), R-interface-compat(A;B), R-frame-compat(A;B), p = q, R-base-domain(R), Rda(R), Rds(R), R-loc(R), R-occurs(R;i;z), @loc: only members of L read x, es realizer ind Rbframe compseq tag def, @loc: k sends only on links in L, es realizer ind Raframe compseq tag def, @loc: k writes only members of L, locl(a), es realizer ind Rpre compseq tag def, @loc precondition for a(v:T):P State(ds) v, source(l), lnk-decl(l;dt), f  g, es realizer ind Rsends compseq tag def, sends knd(v:T) on l:tagged(g,State(ds),v):dt, p q, es realizer ind Reffect compseq tag def, @loc effect knd(v:T) x := f State(ds) v , es realizer ind Rsframe compseq tag def, only events in L send on lnk with tag, <a,b>, es realizer ind Rframe compseq tag def, @loc only events in L change x:T, EqDecider(T), deq-member(eq;x;L), es realizer ind Rnone compseq tag def,  , es realizer ind Rplus compseq tag def, left right, rec(x.A(x)) |